(setf theorems '())

(defmethod claim (p)
  (if (not (member p theorems :test 'equal))
    (setf theorems (cons p theorems))
  )
)

(defmethod disjunction-introduction (p q) ; p -> (p v q)
  (if (member p theorems :test 'equal)
    (progn
      (claim (list p 'v q))
      (claim (list q 'v p))
      (format t "Since ~A is true, by disjunction introduction it is also the case that ~A is true." p (list p 'v q))
    )
  )
)

(defmethod conjunction-elimination (p q) ; (p ^ q) -> p
  (if (or
        (member (list p '^ q) theorems :test 'equal)
        (member (list q '^ p) theorems :test 'equal)
        (and
          (member p theorems :test 'equal)
          (member q theorems :test 'equal)
        )
      )
    (progn
      (claim p)
      (claim q)
      (format t "Since ~A is true, by conjunction elimination it is also the case that ~A and ~A are true." (list p '^ q) p q)
    )
  )
)

(defmethod conjunction (p q) ;((p) ^ (q)) -> (p ^ q)
  (if (or
        (member (list (list p) '^ (list q)) theorems :test 'equal)
        (member (list (list q) '^ (list p)) theorems :test 'equal)
        (and
          (member (list (list p)) theorems :test 'equal)
          (member (list (list q)) theorems :test 'equal)
        )
      )
    (progn
      (claim (list p '^ q))
      (claim (list q '^ p))
      (format t "Since ~A is true, by conjunction it is also the case that ~A is true." (list (list p) '^ (list q)) (list p '^ q))
    )
  )
)

(defmethod modus-ponens (p q) ; (p ^ (p -> q)) -> q
  (if (or 
        (member (list p '^ (list p '-> q)) theorems :test 'equal)
        (member (list (list p '-> q) '^ p) theorems :test 'equal)
        (and
          (member p theorems :test 'equal)
          (member (list p '-> q) theorems :test 'equal)
        )
      )
    (progn
      (claim q)
      (format t "Since ~A is true, by modus ponens it is also the case that ~A is true." (list p '^ (list p '-> q)) q)
    )
  )
)

(defmethod modus-tollens (p q) ; (~q ^ (p -> q)) -> ~p
  (if (or
        (member (list (list '~ q) '^ (list p '-> q)) theorems :test 'equal)
        (member (list (list p '-> q) '^ (list '~ q)) theorems :test 'equal)
        (and
          (member (list '~ q) theorems :test 'equal)
          (member (list p '-> q) theorems :test 'equal)
        )
      )
    (progn
      (claim (list '~ p))
      (format t "Since ~A is true, by modus tollens it is also the case that ~A is true." (list (list '~ q) '^ (list p '-> q)) (list '~ p))
    )
  )
)

(defmethod hypothetical-syllogism (p q r) ; ((p -> q) ^ (q -> r)) -> (p -> r)
  (if (or
        (member (list (list p '-> q) '^ (list q '-> r)) theorems :test 'equal)
        (member (list (list q '-> r) '^ (list p '-> q)) theorems :test 'equal)
        (and 
          (member (list p '-> q) theorems :test 'equal)
          (member (list q '-> r) theorems :test 'equal)
        )
      )
    (progn
      (claim (list p '-> r))
      (format t "Since ~A is true, by hypothetical syllogism it is also the case that ~A is true." (list (list p '-> q) '^ (list q '-> r)) (list p '-> r))
    )
  )
)

(defmethod disjunctive-syllogism (p q) ; ((p v q) ^ ~p) -> q
  (if (or
        (member (list (list p 'v q) '^ (list '~ p)) theorems :test 'equal)
        (member (list (list '~ p) '^ (list p 'v q)) theorems :test 'equal)
        (and 
          (or 
            (member (list p 'v q) theorems :test 'equal)
            (member (list q 'v p) theorems :test 'equal)
            (or 
              (member p theorems :test 'equal)
              (member q theorems :test 'equal)
            )
          )
          (member (list '~ p) theorems :test 'equal)
        )
      )
    (progn
      (claim q)
      (format t "Since ~A is true, by disjunctive syllogism it is also the case that ~A is true." (list (list p 'v q) '^ (list '~ p)) q)
    )
  )
)

(defmethod resolution (p q r) ; ((p v q) ^ (~p v r)) -> (q v r)
  (if (or
        (member (list (list p 'v q) '^ (list (list '~ p) 'v r)) theorems :test 'equal)
        (member (list (list (list '~ p) 'v r) '^ (list p 'v q)) theorems :test 'equal)
        (and 
          (or
            (member (list p 'v q) theorems :test 'equal)
            (member (list q 'v p) theorems :test 'equal)
            (or 
              (member p theorems :test 'equal)
              (member q theorems :test 'equal)
            )
          )
          (or
            (member (list (list '~ p) 'v r) theorems :test 'equal)
            (member (list r 'v (list '~ p)) theorems :test 'equal)
            (or
              (member (list '~ p) theorems :test 'equal)
              (member r theorems :test 'equal)
            )
          )
        )
      )
    (progn
      (claim (list q 'v r))
      (claim (list r 'v q))
      (format t "Since ~A is true, by resolution it is also the case that ~A is true." (list (list p 'v q) '^ (list (list '~ p) 'v r)) (list q 'v r))
    )
  )
)